The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 337 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 15 ms)
    ↳22 CdtProblem
    ↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 46 ms)
    ↳24 CdtProblem
    ↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 47 ms)
    ↳26 CdtProblem
    ↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳30 CdtProblem
    ↳31 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 82 ms)
    ↳32 CdtProblem
    ↳33 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳34 CdtProblem
    ↳35 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 122 ms)
    ↳36 CdtProblem
    ↳37 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳38 CdtProblem
    ↳39 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳40 CdtProblem
    ↳41 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 196 ms)
    ↳42 CdtProblem
↳43 CpxTrsMatchBoundsProof (⇔, 0 ms)
↳44 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(c) → c1(F(g(c)), G(c))
ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(c) → c1(F(g(c)), G(c))
ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c1, c2, c4, c5, c6, c7, c8, c9

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

ACTIVE(c) → c1(F(g(c)), G(c))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c4, c5, c6, c7, c8, c9

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
We considered the (Usable) Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = x1   
POL(active(x1)) = x1   
POL(c) = [2]   
POL(c2(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [1]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = x1   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c4, c5, c6, c7, c8, c9

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(f(z0)) → c4(F(proper(z0)), PROPER(z0)) by

PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c4

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c4
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(f(x0)) → c4
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4, c4

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

PROPER(f(x0)) → c4

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, PROPER, F, G, TOP

Compound Symbols:

c2, c5, c6, c7, c8, c9, c4

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(g(z0)) → c5(G(proper(z0)), PROPER(z0)) by

PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c5

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c5
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(g(x0)) → c5
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c5, c5

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

PROPER(g(x0)) → c5

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c8, c9, c4, c5

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0)) by

TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(x0)) → c8

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(mark(x0)) → c8
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(mark(z0)) → c8(TOP(proper(z0)), PROPER(z0))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c9, c4, c5, c8, c8

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

TOP(mark(x0)) → c8

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, TOP, PROPER

Compound Symbols:

c2, c6, c7, c9, c4, c5, c8

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace TOP(ok(z0)) → c9(TOP(active(z0)), ACTIVE(z0)) by

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
K tuples:none
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c9

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(ok(x0)) → c9
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4] + [4]x1   
POL(g(x1)) = [1] + [3]x1   
POL(mark(x1)) = [4]   
POL(ok(x1)) = [5]   
POL(proper(x1)) = [2]x1   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
K tuples:

TOP(ok(x0)) → c9
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c9

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [2]x1   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = 0   
POL(g(x1)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = [2] + [4]x1   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
S tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
K tuples:

TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c9

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = [4]   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = 0   
POL(TOP(x1)) = [4]x1   
POL(c) = [5]   
POL(c2(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9) = 0   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4]   
POL(g(x1)) = 0   
POL(mark(x1)) = x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(c)) → c4(F(ok(c)), PROPER(c))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c9

(27) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(f(c)) → c4(F(ok(c)), PROPER(c)) by

PROPER(f(c)) → c4(F(ok(c)))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
TOP(ok(x0)) → c9
PROPER(f(c)) → c4(F(ok(c)))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
K tuples:

TOP(ok(x0)) → c9
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c9, c4

(29) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

TOP(ok(x0)) → c9

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(c)) → c4(F(ok(c)))
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c4

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

PROPER(f(c)) → c4(F(ok(c)))
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = [4]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [2]   
POL(g(x1)) = 0   
POL(mark(x1)) = [2] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0)))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c4

(33) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(f(f(z0))) → c4(F(f(proper(z0))), PROPER(f(z0))) by

PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c4, c4

(35) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

PROPER(f(f(x0))) → c4
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [1]   
POL(TOP(x1)) = x1   
POL(c) = [5]   
POL(c2(x1)) = x1   
POL(c4) = 0   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [4]   
POL(g(x1)) = 0   
POL(mark(x1)) = [1] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0)))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c4, c5, c8, c9, c4, c4

(37) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace PROPER(f(g(z0))) → c4(F(g(proper(z0))), PROPER(g(z0))) by

PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(f(x0))) → c4
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c5, c8, c9, c4, c4, c4

(39) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

PROPER(f(f(x0))) → c4

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c5, c8, c9, c4, c4, c4

(41) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

PROPER(f(g(x0))) → c4
We considered the (Usable) Rules:

proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
g(ok(z0)) → ok(g(z0))
f(ok(z0)) → ok(f(z0))
And the Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(ACTIVE(x1)) = 0   
POL(F(x1)) = 0   
POL(G(x1)) = 0   
POL(PROPER(x1)) = [4]   
POL(TOP(x1)) = [4]x1   
POL(c) = [4]   
POL(c2(x1)) = x1   
POL(c4) = 0   
POL(c4(x1)) = x1   
POL(c4(x1, x2)) = x1 + x2   
POL(c5(x1, x2)) = x1 + x2   
POL(c6(x1)) = x1   
POL(c7(x1)) = x1   
POL(c8(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(f(x1)) = [2]   
POL(g(x1)) = 0   
POL(mark(x1)) = [2] + x1   
POL(ok(x1)) = x1   
POL(proper(x1)) = 0   

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

active(c) → mark(f(g(c)))
active(f(g(z0))) → mark(g(z0))
proper(c) → ok(c)
proper(f(z0)) → f(proper(z0))
proper(g(z0)) → g(proper(z0))
f(ok(z0)) → ok(f(z0))
g(ok(z0)) → ok(g(z0))
top(mark(z0)) → top(proper(z0))
top(ok(z0)) → top(active(z0))
Tuples:

ACTIVE(f(g(z0))) → c2(G(z0))
F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
TOP(mark(c)) → c8(TOP(ok(c)), PROPER(c))
TOP(mark(f(z0))) → c8(TOP(f(proper(z0))), PROPER(f(z0)))
TOP(mark(g(z0))) → c8(TOP(g(proper(z0))), PROPER(g(z0)))
TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
PROPER(f(g(x0))) → c4
S tuples:

F(ok(z0)) → c6(F(z0))
G(ok(z0)) → c7(G(z0))
PROPER(g(c)) → c5(G(ok(c)), PROPER(c))
PROPER(g(f(z0))) → c5(G(f(proper(z0))), PROPER(f(z0)))
PROPER(g(g(z0))) → c5(G(g(proper(z0))), PROPER(g(z0)))
PROPER(f(f(c))) → c4(F(f(ok(c))), PROPER(f(c)))
PROPER(f(f(f(z0)))) → c4(F(f(f(proper(z0)))), PROPER(f(f(z0))))
PROPER(f(f(g(z0)))) → c4(F(f(g(proper(z0)))), PROPER(f(g(z0))))
PROPER(f(g(c))) → c4(F(g(ok(c))), PROPER(g(c)))
PROPER(f(g(f(z0)))) → c4(F(g(f(proper(z0)))), PROPER(g(f(z0))))
PROPER(f(g(g(z0)))) → c4(F(g(g(proper(z0)))), PROPER(g(g(z0))))
K tuples:

TOP(ok(c)) → c9(TOP(mark(f(g(c)))), ACTIVE(c))
ACTIVE(f(g(z0))) → c2(G(z0))
TOP(ok(f(g(z0)))) → c9(TOP(mark(g(z0))), ACTIVE(f(g(z0))))
PROPER(f(c)) → c4(F(ok(c)))
PROPER(f(g(x0))) → c4
Defined Rule Symbols:

active, proper, f, g, top

Defined Pair Symbols:

ACTIVE, F, G, PROPER, TOP

Compound Symbols:

c2, c6, c7, c5, c8, c9, c4, c4, c4

(43) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 6.
The certificate found is represented by the following graph.
Start state: 2513
Accept states: [2514, 2515, 2516, 2517, 2518]
Transitions:
2513→2514[active_1|0]
2513→2515[proper_1|0]
2513→2516[f_1|0]
2513→2517[g_1|0]
2513→2518[top_1|0]
2513→2513[c|0, mark_1|0, ok_1|0]
2513→2519[c|1]
2513→2522[c|1]
2513→2523[f_1|1]
2513→2524[g_1|1]
2513→2525[active_1|1]
2513→2526[proper_1|1]
2513→2529[c|2]
2513→2535[c|2]
2513→2539[c|3]
2513→2551[c|4]
2519→2520[g_1|1]
2519→2533[proper_1|2]
2520→2521[f_1|1]
2520→2532[proper_1|2]
2521→2514[mark_1|1]
2521→2525[mark_1|1]
2521→2527[proper_1|2]
2522→2515[ok_1|1]
2522→2526[ok_1|1]
2522→2528[active_1|2]
2523→2516[ok_1|1]
2523→2523[ok_1|1]
2524→2517[ok_1|1]
2524→2524[ok_1|1]
2525→2518[top_1|1]
2526→2518[top_1|1]
2527→2518[top_1|2]
2528→2518[top_1|2]
2529→2530[g_1|2]
2529→2537[proper_1|3]
2530→2531[f_1|2]
2530→2536[proper_1|3]
2531→2528[mark_1|2]
2531→2534[proper_1|3]
2532→2527[f_1|2]
2533→2532[g_1|2]
2534→2518[top_1|3]
2535→2533[ok_1|2]
2535→2538[g_1|3]
2535→2543[g_1|4]
2535→2547[proper_1|5]
2536→2534[f_1|3]
2537→2536[g_1|3]
2538→2532[ok_1|3]
2538→2540[f_1|3]
2539→2537[ok_1|3]
2539→2541[g_1|4]
2539→2548[g_1|5]
2539→2547[ok_1|3]
2539→2550[proper_1|6]
2540→2527[ok_1|3]
2540→2542[active_1|3]
2541→2536[ok_1|4]
2541→2544[f_1|4]
2541→2545[ok_1|4]
2541→2552[active_1|5]
2542→2518[top_1|3]
2543→2542[mark_1|4]
2543→2545[proper_1|4]
2544→2534[ok_1|4]
2544→2546[active_1|4]
2545→2518[top_1|4]
2546→2518[top_1|4]
2547→2545[g_1|5]
2548→2546[mark_1|5]
2548→2549[proper_1|5]
2549→2518[top_1|5]
2550→2549[g_1|6]
2551→2550[ok_1|4]
2551→2553[g_1|5]
2552→2518[top_1|5]
2553→2549[ok_1|5]
2553→2554[active_1|6]
2554→2518[top_1|6]

(44) BOUNDS(O(1), O(n^1))